// Sub_menu の差別化

function do_menu() {
	if (window.parent != window) {
		var id = window.parent.bold_menu && window.parent.bold_menu();
		var elem = id && document.getElementById(id);
		if (elem) {
			elem.style.fontWeight = 'bold';
		}
	}
}
